\begin{tabbing}
sframe{-}p(${\it es}$; $l$; ${\it tg}$; $L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (es{-}kind(${\it es}$; es{-}sender(${\it es}$; $e$)) $\in$ $L$ $\in$ Knd)
\-
\end{tabbing}